PET

Benchmark
Model:pacman v.1 (MDP)
Parameter(s)MAXSTEPS = 100
Property:crash (prob-reach)
Invocation (specific)
./smc.sh pacman.nm pacman.props -prop crash -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams S:50000000,Av:10,e:0.05,d:0.05,p:0.05,post:64 -const MAXSTEPS=100
Execution
Walltime:663.4088761806488s
Return code:1
Log
PRISM-games
===========

Version: 2.0.beta3
Date: Fri Mar 20 05:12:32 UTC 2020
Hostname: 68eec9c801d9
Memory limits: cudd=1g, java(heap)=8.9g
Command line: prism pacman.nm pacman.props -prop crash -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams 'S:50000000;Av:10;e:0.05;d:0.05;p:0.05;post:64' -const MAXSTEPS=100 -javamaxmem 10g

Parsing the model file "pacman.nm"...

Parsing properties file "pacman.props"...

1 property:
(1) "crash": Pmin=? [ F "Crash" ]

Type:        MDP
Modules:     arbiter ghost0 ghost1 pacman 
Variables:   pMove steps xG0 yG0 dG0 xG1 yG1 dG1 xP yP dP 

---------------------------------------------------------------------

Model checking: "crash": Pmin=? [ F "Crash" ]
Model constants: MAXSTEPS=100
Starting heuristic: RTDP_ADJ
IsMDP false Collapse false break false
ColourParams: S:50000000 Av: 10 eps: 0.05 delta: 0.05 pmin: 0.05
TransDelta: 2.583673656205288E-11
HeuristicSG: Version try0
Grey
======================================
STDERR
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.Arrays.copyOf(Arrays.java:3308)
	at java.util.BitSet.ensureCapacity(BitSet.java:337)
	at java.util.BitSet.expandTo(BitSet.java:352)
	at java.util.BitSet.set(BitSet.java:447)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:187)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)
	at explicit.SCCComputerTarjan.tarjan(SCCComputerTarjan.java:175)